module Zeno.Clause where

import Prelude ()
import StdImports
import Zeno.Term
import Traversing
import qualified Data.Set as Set

data Quantified f a
  = Quantified  { quantifiedVariables :: ![a],
                  quantifiedObject :: !(f a) }
  deriving ( Eq, Ord, Functor, Foldable, Traversable )

data Clause a
  = Clause      { clauseEquality :: !(Equality a),
                  clauseConditions :: ![Equality a] }
  deriving ( Eq, Ord, Functor, Foldable, Traversable )
  
data Equality a 
  = Equals      { equalityLeft :: !(Term a),
                  equalityRight :: !(Term a) }
  deriving ( Eq, Ord, Functor, Foldable, Traversable )

flipEquality :: Equality a -> Equality a 
flipEquality (Equals l r) = Equals r l

equalityToPair :: Equality a -> (Term a, Term a)
equalityToPair (Equals l r) = (l, r)

pairToEquality :: (Term a, Term a) -> Equality a
pairToEquality = uncurry Equals

equalitiesToSubstitution :: Ord a => [Equality a] -> TermSubstitution a
equalitiesToSubstitution = Set.fromList . map equalityToPair
  
flipClauseEquality :: Clause a -> Clause a
flipClauseEquality cs = cs 
  { clauseEquality = flipEquality (clauseEquality cs) }
  
flipQuantifiedClauseEquality :: Quantified Clause a -> Quantified Clause a
flipQuantifiedClauseEquality q = q
  { quantifiedObject = flipClauseEquality (quantifiedObject q) }

addCondition :: Equality a -> Clause a -> Clause a
addCondition eq cs = cs 
  { clauseConditions = eq : (clauseConditions cs) }
  
instance WithinTraversable (Term a) (Equality a) where
  mapWithinM f (t1 `Equals` t2) = do
    t1' <- mapWithinM f t1
    t2' <- mapWithinM f t2
    return (t1' `Equals` t2')
  
instance WithinTraversable (Term a) (Clause a) where
  mapWithinM f (Clause eq conds) = do
    eq' <- mapWithinM f eq
    conds' <- mapM (mapWithinM f) conds
    return (Clause eq' conds')
    
instance WithinTraversable c (a b) => 
         WithinTraversable c (Quantified a b) where
  mapWithinM f (Quantified vars obj) = do
    obj' <- mapWithinM f obj
    return (Quantified vars obj')
    
instance Show a => Show (Equality a) where
  show (Equals l r) = 
    case r' of
      "True" -> l'
      "False" ->
        if ' ' `elem` l' 
          then "not (" ++ l' ++ ")"
          else "not " ++ l'
      _ -> l' ++ " = " ++ r'
    where
      (l', r') = (show l, show r)
      
instance Show a => Show (Clause a) where
  show (Clause t cs) = 
    let cs_s = case cs of
          [] -> ""
          cs -> " :- " 
            ++ intercalate ", " (map show cs)
    in show t ++ cs_s
    
instance (Show b, Show (a b)) => Show (Quantified a b) where
  show (Quantified vars obj) = 
    case vars of
      [] -> show obj
      _ -> "forall " ++ (intercalate ", " $ map show vars) 
        ++ " . " ++ show obj
